7.1 KB · ⇊ 5 parts · ⤓ Micron 7.1 KB · ⤓ HTML 17.4 KB

top

The CADE ATP System Competition (CASC) is an annual competition of fully automated theorem provers for classical logiccite-ref-1[1]cite-ref-2[2]cite-ref-stateofcasc-3-0[3]cite-ref-4[4]

• Competition

• See also

• References

• External links

CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated Reasoning. It has inspired similar competition in related fields, in particular the successful SMT-COMP competitioncite-ref-5[5] for satisfiability modulo theories, the SAT Competitioncite-ref-6[6] for propositional reasoners, and the modal logic reasoning competition.cite-ref-7[7]

The first CASC, CASC-13, was held as part of the 13th Conference on Automated Deduction at Rutgers University, New Brunswick, NJ, in 1996.cite-ref-stateofcasc-3-1[3] Among the systems competing were Ottercite-ref-8[8] and SETHEO.cite-ref-9[9]

• List of computer science awards

cite-note-11. ↑ citerefsutcliffe2011Sutcliffe, Geoff (2011). "The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5". AI Communications. 24 (1): 75–89. doi:10.3233/AIC-2010-0483.

cite-note-22. ↑ citerefgeoff-sutcliffeGeoff Sutcliffe. "The CADE ATP System Competition". Archived from the original on 2009-03-02. Retrieved 2008-10-23.

cite-note-stateofcasc-33. ↑ citerefgeoff-sutcliffe-and-christian-suttner2006Geoff Sutcliffe and Christian Suttner (2006). "The State of CASC". AI Communications. 19 (1): 35–48.

cite-note-44. ↑ citerefjeff-pelletier-geoff-sutcliffe-and-christian-suttner2002Jeff Pelletier, Geoff Sutcliffe and Christian Suttner (2002). "The Development of CASC" (PDF). AI Communications. 15 (2–3): 79–90.

cite-note-55. ↑ citerefbarrettde-mourastump2005Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Satisfiability Modulo Theories Competition" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. 3576. Springer: 20–23. doi:10.1007/11513988_4. ISBN 978-3-540-27231-1.

cite-note-66. ↑ citerefmattile-berrerousselsimon2012Matti, Järvisalo; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012). "The international SAT solver competitions". AI Magazine. 33 (1): 89–92. doi:10.1609/aimag.v33i1.2395.

cite-note-77. ↑ citerefmassaccidonini2000Massacci, Fabio; Donini, Francesco M. (2000). "Design and results of TANCS-2000 non-classical (modal) systems comparison". International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science. 1847. Springer: 52–56. CiteSeerX 10.1.1.385.6267. doi:10.1007/10722086_4. ISBN 978-3-540-67697-3.

cite-note-88. ↑ citerefmccunewos1997McCune, William; Wos, Larry (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning. 18 (2): 211–220. doi:10.1023/A:1005843632307. S2CID 2481653.

cite-note-99. ↑ citerefmoseribensletzsteinbach1997Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning. 18 (2): 237–246. doi:10.1023/A:1005808119103. S2CID 821198.

• Archive of original CASC website

• CASC Website